// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#include <stddef.h>
#include <sHT/index.h>
#include <sHT/lex/nat.h>
#include <sHT/logic/arithmetic.h>
#include <sHT/logic/failbit.h>

#define sHT_ascii_zero 0x30u

/* Used e.g. for parsing port numbers, IPv4 octets ... */

/* TODO: Eligible to optimisation.

  - different lengths: IPv4 octets: 127, 0, 1, 20 are never out-of-bounds
  - SIMD: allowing for some bugs, this can sometimes be done branchless!
    (https://stackoverflow.com/questions/31679341/,
    https://stackoverflow.com/questions/35127060)
  - `sHT_findchar`, followed Duff's device

  ... but profile first */

struct sHT_decimal_u32
sHT_decimal_u32_c1(size_t length, const unsigned char from[], uint_least32_t first)
{
	sHT_overflowing
	uint_least32_t val = first;
	/* invariant, nonspec: good(size_t, overflow) ↔ val ∈ \bounds(val),
	   invariant: fail_value(size_t, overflow) = 0

	  First: good(size_t, overflow), val ∈ \bounds(val).
	  Second: fail_value(size_t, overflow) = 0  */
	sHT_with_failbit
	size_t overflow = sHT_success(0);

	size_t i = 1;
	/* TODO: optimise for small `length` (especially 127.0.0.1)? */
	/* loop invariants:
	  (A) nonspec: val = sum (k <- 0 \to i) (d(k) * exp(10, i - k - 1))
	  (B) nonspec: match decimal* from 1 i

	  base case (i = 1):
	  sum (k <- 0 \to 1) (d(k) * exp(10, i - k - 1))
	    = d(0) * exp(10, 1 - 0 - 1)
	    = d(0)
	    = first
	    = (A) val
	  (B) ⇔ match _* from 1 1 ⇔ ⊤ */
	sHT_index_continue(i, length) {
		/* (sHT_index_continue) ⇒ (1) 0 ≤ i < length ∨ i = 0
		  (b) ⇒ (2) 0 < length
		  (1, 2) ⇒ (3) 0 ≤ i < length
		  (a, 3) ⇒ (read ^ set) from[i] */
		uint_least32_t c = from[i];
		/* Strictly speaking, these are branches,
		  but GCC would have a hard time using this information */
		if ((c -= sHT_ascii_zero) > 9)
			/* nonspec: c ∉ decimal ⇒ (C) from[i] ∉ decimal

			  nonspec: (B, C) ⇒ maximalise k : { k | 1 ≤ k ≤ length },
			    match decimal* from 1 k = i
			  ⇒ (F) end = i */
			break;
		/* nonspec: c ∈ decimal ⇒ (C) from[i] ∈ decimal */
		/* (B, C) ⇒ (D) match decimal* from 1 (i + 1) */

		/*
		good(new overflow) := good(old overflow) ∧ (10 * old val + c ∈ \bounds(val))
		  = (overflow) old val ∈ \bounds(val) ^ (10 * old val + c ∈ \bounds(val))
                  = 10 * old val + c ∈ \bounds(val) (c ≥ 0)
		  = new val ∈ \bounds(val)
		(overflow invariant)

		nonspec: val := 10 * old val + d(i)
		  = 10 * sum (k <- 0 \to i) (d(k) * exp(10, i - k - 1)) + d(i) (a)
		  = sum (k <- 0 \to i) (10 * d(k) * exp(10, i - k - 1)) + d(i)
		  = sum (k <- 0 \to i) (d(k) * exp(10, i - k)) + d(i)
		  = sum (k <- 0 \to i) (d(k) * exp(10, i - k)) + d(i) * exp(10, i - i)
		  = (E) sum (k <- 0 \to i + 1) (d(k) * exp(10, i - k)) */
		sHT_muladd_overflow(uint_least32_t, &val, 10u, val, c, &overflow);
		/* loop increment: rewrite (E, D) into (A, B) */
	}
	/* * Normal exit:
	   nonspec: (G) i = length
	   (H) 0 ≤ i ≤ length ∨ i = 0

	   nonspec: (B) match decimal* from 1 i
	   nonspec: (G, B) ⇒ match decimal* from 1 length
	     ⇒ maximalise k : { k | 1 ≤ k ≤ length } = length
	     ⇒ end = length
	     ⇒ (F) end = i (G)

	   * Break (proofs above)
	   (F) nonspec: end = i
	   (H) 0 ≤ i ≤ length ∨ i = 0 (sHT_index_continue)

	   * Always
	   (H, b) ⇒ (I) 0 ≤ i < length */
	/* Begin sHT_transfer_failure

	   Requires:
	   (overflow invariant)
	     ⇒ %a
	   (I, b)
	     ⇒ 0 < i < failbit_limit(size_t)
	     ⇒ %b

	   Ensures:
	   %z ⇒ (1) fail_value(size_t, ret.end) := i
	   %y ⇒ (2) good(size_t, ret.end) := good(overflow)

	   End

	   nonspec: (A, F)
	     ⇒ val = sum (k <- 0 \to end) (d(k) * exp(10, i - k - 1))
	     ⇒ val = string->nat end d
	     ⇒ (z) val = value (by definition of value)

	   (1, I) ⇒ (w) 0 ≤ fail_value(size_t, ret.end) < length 0 ≤ i
	   nonspec: (1, F) ⇒ (x) fail_value(size_t, ret.end) = end
	   nonspec: (2, overflow invariant)
	     ⇒ (4) good(size_t, ret.end) ↔ val ∈ \bounds(val)
           nonspec: (3, 4) ⇒ (y) */
	size_t end = sHT_transfer_failbit_novalue(overflow, i);
	return (struct sHT_decimal_u32) { .val = val, .end = end };
}
